i:Id. onceR{a:ut2, done:ut2}(i)  Realizer 

latex

Definitions	onceR{$a:ut2, $done:ut2}(i), if b t else f fi, s.x, true, Top, DeclaredType(ds;x), x:A. B(x), Prop, x. t(x), t  T, Id, x(s), State(ds)
Lemmas	Rframe wf, locl wf, subtype rel self, fpf-single wf, eqof eq btrue, Rlist wf, id-deq wf, Rpre wf, Reffect wf, btrue wf, fpf-cap-single1, Id wf, Rinit wf, fpf-cap-single